In all of these cases, the designer will implement the logic in a way that is intended to match the asserted behavior. But designers sometimes make mistakes, and so the assertion provides a crosscheck that can warn when the design's behavior differs from the behavior specified by the assertion. If the assertion is ever violated during Verilog simulation, then it is highly desirable if this violation can be detected and reported.

Beyond simulation, assertions can also be the targets for formal and semiformal verification tools. These tools build formal, mathematical models of the design and use reasoning techniques to prove or disprove properties of the design's intended behavior.

If the tool discovers a way to violate a property, then it has found a bug in the design. If the tool can prove that there is no way to ever violate a property, then this is valuable verification information.

In the examples above, a formal or semiformal tool might be able to prove that there is no way that two Verilog case items can ever evaluate in parallel or that there is no way that a state machine can ever make an illegal transition, and so forth. It is highly desirable that any formal-based verification tool target properties matching assertions used in simulation. This allows assertions to be specified and debugged in simulation before being used with formal methods. Further, if the simulation test suite contains a test that violates an assertion, this indicates a design bug that should be fixed before running formal analysis.

Assertions in a design are good examples of "white-box" verification since they can specify intended internal behavior of a design and not just end-to-end behavior from design inputs to design outputs. In many cases, including several of the examples above, assertions map directly to internal design structures such as state machines and memories.

In addition to checking for problems that may indicate design bugs, assertions on internal structures improve overall design observability and visibility into design behavior. From the outputs of a large design, it can be hard to detect the effects of a deeply buried bug and very time-consuming to diagnose and fix the bug. It is better to detect the bug at the source, or closer to the source, at the point where an assertion on an internal design structure reports a violation.

Basic Verilog assertions

The most basic way to specify an assertion within a Verilog design is to add a comment. For example, consider the one-hot state register discussed earlier. The following code shows the addition of a comment to document the designer's belief that the encoding will always be one-hot.

// This state register should always be one_hot

Using a comment to document something important about the design is always a good thing for a designer to do, regardless of whether the comment is written in the form of an executable assertion. A comment-based assertion documents a designer's assumptions and makes it easier for another engineer to understand what the design is supposed to do.

The drawback of a comment, of course, is that it is only a comment and therefore provides no automatic checking during simulation. For this reason, designers sometimes include extra Verilog code to check the assumption and report any violations with a Verilog $display statement. Usually, the designer wants this code to be active during simulation but not actually synthesized into the logic. Some designers ignore this issue, and count on their logic synthesis tool to prune away logic that cannot affect any module outputs.

Other designers consider this approach too risky and instead use synthesis off/on comment-based pragmas or some other form of conditional compilation around the assertion checking code to be sure that it is not synthesized. Additional pragmas may be needed so that other RTL analysis tools, such as code coverage, also ignore the checking logic.

Here is an example of one-hot assertion checking logic included in the Verilog code. Even this simple assertion raises several issues.

reg [3:0] state_var;
.
//synopsys translate_off
integer idx, ones_found;
always @(state_var)
begin
ones_found = 0;
for (idx = 0; idx < 4 ; idx = idx + 1)
if (state_var[idx] === 1'b1)
ones_found = ones_found + 1;
if (ones_found != 1)
$display("one_hot violation at %d",$time);
end
//synopsys translate_on

Two new variables (ones_found and idx) have been added to the module just to support the checking logic. The check is closely linked to the design itself.

If, for example, the designer were to rename the state_var register then several changes would also be required for the checking logic. Such ripple effects from RTL changes can be a major issue for more complex assertion checks that may require dozens or even hundreds of lines of Verilog code.

This simple example ignores a number of details. For example, this implementation checks only the number of 1'b1 bits and ignores whether the other bits are 1'b0, unknown (1'bx) or even tri-stated (1'bz). More checking logic is needed if the designer wants to report a violation for values of state_var such as 4'b0x10. Special handling may also be needed around the reset pulse; for example, state_var might come out of reset with a value of 4'b0000 and only start loading one-hot values after the first clock. Quite often, what appears to be a simple assertion check turns out to require considerable effort on the part of the designer.

The use of in-line Verilog checking logic provides no verification reuse. The designer may end up cutting and pasting large blocks of code to perform similar checks in different places. A change in design assumptions may then require changes in multiple locations in the code. This method also provides no verification reuse when moving from simulation to formal or semiformal verification; in general, a formal-based tool cannot determine the properties to be verified given only $display statements mixed in with synthesizable and non-synthesizable Verilog code.

Verilog assertion libraries

The most obvious way to specify Verilog assertions while fostering verification reuse is to use a library of common assertion checkers, such as the recently introduced Open Verification Library (OVL). Often, assertions linked to specific design structures can be used in multiple locations within the RTL code. Capturing these common assertions in the form of Verilog modules enables reuse whenever the same assertion check is appropriate. Some of the complex issues described earlier, such as special handling around resets, can be solved once in the library module and then leveraged wherever the module is instantiated.

Further, the designer can accommodate some types of RTL changes without much effort. When a variable name changes, the designer can generally change just the variable used in the module instantiation rather than making multiple changes in the assertion checking code itself. This is a significant advantage relative to specifying the assertion with in-line Verilog checking logic.

OVL defines a library of Verilog "monitor" modules that can be instantiated at appropriate places in the RTL of the design to represent assertions. OVL monitors perform assertion checks as the simulation runs and report violations. The OVL initiative also has a goal of making the assertions in the library easily targeted by formal verification tools.

Here is an example of using an OVL module instantiation to check one-hot encoding of a state register. The monitor module contains synthesis translate off/on pragmas around the checking logic, so the designer usually does not need to include special constructs to ensure that the checking logic is not synthesized.

The advantages of an assertion-checking library over explicit in-line Verilog code are clear, but this method has substantial limitations of its own. For example, this assertion style does not allow assertions to be placed in-context within the RTL code. Consider the case of an assertion that is only valid-and should only be checked-when certain conditions are true. If the conditions are already expressed within the RTL, for example with a Verilog if statement, then it is important to leverage these conditions when specifying the checker.

In-context conditioning, in which different assertion checks are performed depending upon the surrounding RTL, is available with in-line Verilog checking logic.

Different checks can be placed within the if and else clauses so that each is active only when the corresponding if or else condition is true. In-context assertions cannot be expressed using assertion libraries such as OVL; Verilog syntax rules do not permit module instantiations at arbitrary points within the RTL. This often means that design logic must be replicated as part of the checking logic to provide appropriate conditioning.

Another limitation of using Verilog module instantiations for assertion checking is the lack of flexibility of the argument syntax. Although Verilog parameters provide some flexibility, for example in variable widths, Verilog module instantiations do not allow easy specification of a variable number of optional arguments with default argument values. In general, every argument must be explicitly specified in each instantiation of a Verilog assertion library element.

Assertion libraries do not necessarily need to be written in Verilog; some people write their assertions in C or in other testbench languages and link the assertions to Verilog via the PLI interface. The use of PLI-based calls permits a more flexible syntax than Verilog module instantiations. The downside is that PLI is inherently an inefficient interface, so assertion checks of this type generally add an unacceptable level of overhead to simulation.

Checker directives

The most flexible method for specifying assertion checks in Verilog is to use a comment-based directive syntax to invoke elements from an assertion checker library. The use of comments means that no synthesis off/on pragmas or other special handling is needed to make the assertions transparent to logic synthesis and other tools. The freedom from Verilog module instantiation syntax enables in-context specification and a high degree of flexibility in the number of arguments.

More importantly, an intelligent checker generation tool combines information in the checker directive and in the design RTL to produce checking code that is highly tailored to fit the specific design. The code below is an example of a one-hot assertion. It is hard to imagine a simpler way to specify assertions; any relevant clocks and resets and even the variable to be checked can be inferred from the register declaration on the same line as the directive. A checker generation tool can read the RTL file containing this directive and then generate a properly configured one-hot checker for state_var that will work in simulation and report any violations.

reg [3:0] state_var; //assertion one_hot

This also demonstrates another advantage of assertion libraries; well-chosen directive names help to make the design self-documenting. The use of an assertion named one_hot rather than in-line Verilog code makes the assertion much more understandable for an engineer who has to read and comprehend the RTL.

The power of the checker directive approach combined with an intelligent checker generation tool allows the checkers to adapt to changes in the RTL. All three directives shown above are identical, yet a checker generation tool will product different checkers because the names and widths of the state registers to be checked are inferred from the RTL. Therefore, common changes in the RTL do not require any changes in the checker directives.

Because of these advantages, 0-In Design Automation selected a checker directive approach when developing its white-box verification suite. Checker directives make it very easy for designers to specify assertions as they write their Verilog RTL code. 0-In's comment-based directives reference the 0-In CheckerWare library, which includes: